(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(X)
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X
Rewrite Strategy: FULL
(1) RenamingProof (EQUIVALENT transformation)
Renamed function symbols to avoid clashes with predefined symbol.
(2) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
from(X) → cons(X, n__from(s(X)))
length(n__nil) → 0'
length(n__cons(X, Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from(X) → n__from(X)
nil → n__nil
cons(X1, X2) → n__cons(X1, X2)
activate(n__from(X)) → from(X)
activate(n__nil) → nil
activate(n__cons(X1, X2)) → cons(X1, X2)
activate(X) → X
S is empty.
Rewrite Strategy: FULL
(3) SlicingProof (LOWER BOUND(ID) transformation)
Sliced the following arguments:
from/0
cons/0
n__from/0
n__cons/0
(4) Obligation:
Runtime Complexity Relative TRS:
The TRS R consists of the following rules:
from → cons(n__from)
length(n__nil) → 0'
length(n__cons(Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from → n__from
nil → n__nil
cons(X2) → n__cons(X2)
activate(n__from) → from
activate(n__nil) → nil
activate(n__cons(X2)) → cons(X2)
activate(X) → X
S is empty.
Rewrite Strategy: FULL
(5) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)
Infered types.
(6) Obligation:
TRS:
Rules:
from → cons(n__from)
length(n__nil) → 0'
length(n__cons(Y)) → s(length1(activate(Y)))
length1(X) → length(activate(X))
from → n__from
nil → n__nil
cons(X2) → n__cons(X2)
activate(n__from) → from
activate(n__nil) → nil
activate(n__cons(X2)) → cons(X2)
activate(X) → X
Types:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
(7) OrderProof (LOWER BOUND(ID) transformation)
Heuristically decided to analyse the following defined symbols:
length,
length1They will be analysed ascendingly in the following order:
length = length1
(8) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
length1, length
They will be analysed ascendingly in the following order:
length = length1
(9) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
length1(
gen_n__from:n__nil:n__cons3_0(
+(
1,
n6_0))) →
*5_0, rt ∈ Ω(n6
0)
Induction Base:
length1(gen_n__from:n__nil:n__cons3_0(+(1, 0)))
Induction Step:
length1(gen_n__from:n__nil:n__cons3_0(+(1, +(n6_0, 1)))) →RΩ(1)
length(activate(gen_n__from:n__nil:n__cons3_0(+(1, +(n6_0, 1))))) →RΩ(1)
length(gen_n__from:n__nil:n__cons3_0(+(2, n6_0))) →RΩ(1)
s(length1(activate(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))))) →RΩ(1)
s(length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0)))) →IH
s(*5_0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(10) Complex Obligation (BEST)
(11) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Lemmas:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))) → *5_0, rt ∈ Ω(n60)
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
length
They will be analysed ascendingly in the following order:
length = length1
(12) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
length(
gen_n__from:n__nil:n__cons3_0(
+(
1,
n2063_0))) →
*5_0, rt ∈ Ω(n2063
0)
Induction Base:
length(gen_n__from:n__nil:n__cons3_0(+(1, 0)))
Induction Step:
length(gen_n__from:n__nil:n__cons3_0(+(1, +(n2063_0, 1)))) →RΩ(1)
s(length1(activate(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0))))) →RΩ(1)
s(length1(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0)))) →RΩ(1)
s(length(activate(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0))))) →RΩ(1)
s(length(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0)))) →IH
s(*5_0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(13) Complex Obligation (BEST)
(14) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Lemmas:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))) → *5_0, rt ∈ Ω(n60)
length(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0))) → *5_0, rt ∈ Ω(n20630)
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
The following defined symbols remain to be analysed:
length1
They will be analysed ascendingly in the following order:
length = length1
(15) RewriteLemmaProof (LOWER BOUND(ID) transformation)
Proved the following rewrite lemma:
length1(
gen_n__from:n__nil:n__cons3_0(
+(
1,
n4016_0))) →
*5_0, rt ∈ Ω(n4016
0)
Induction Base:
length1(gen_n__from:n__nil:n__cons3_0(+(1, 0)))
Induction Step:
length1(gen_n__from:n__nil:n__cons3_0(+(1, +(n4016_0, 1)))) →RΩ(1)
length(activate(gen_n__from:n__nil:n__cons3_0(+(1, +(n4016_0, 1))))) →RΩ(1)
length(gen_n__from:n__nil:n__cons3_0(+(2, n4016_0))) →RΩ(1)
s(length1(activate(gen_n__from:n__nil:n__cons3_0(+(1, n4016_0))))) →RΩ(1)
s(length1(gen_n__from:n__nil:n__cons3_0(+(1, n4016_0)))) →IH
s(*5_0)
We have rt ∈ Ω(n1) and sz ∈ O(n). Thus, we have ircR ∈ Ω(n).
(16) Complex Obligation (BEST)
(17) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Lemmas:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n4016_0))) → *5_0, rt ∈ Ω(n40160)
length(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0))) → *5_0, rt ∈ Ω(n20630)
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(18) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n4016_0))) → *5_0, rt ∈ Ω(n40160)
(19) BOUNDS(n^1, INF)
(20) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Lemmas:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n4016_0))) → *5_0, rt ∈ Ω(n40160)
length(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0))) → *5_0, rt ∈ Ω(n20630)
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(21) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n4016_0))) → *5_0, rt ∈ Ω(n40160)
(22) BOUNDS(n^1, INF)
(23) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Lemmas:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))) → *5_0, rt ∈ Ω(n60)
length(gen_n__from:n__nil:n__cons3_0(+(1, n2063_0))) → *5_0, rt ∈ Ω(n20630)
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(24) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))) → *5_0, rt ∈ Ω(n60)
(25) BOUNDS(n^1, INF)
(26) Obligation:
TRS:
Rules:
from →
cons(
n__from)
length(
n__nil) →
0'length(
n__cons(
Y)) →
s(
length1(
activate(
Y)))
length1(
X) →
length(
activate(
X))
from →
n__fromnil →
n__nilcons(
X2) →
n__cons(
X2)
activate(
n__from) →
fromactivate(
n__nil) →
nilactivate(
n__cons(
X2)) →
cons(
X2)
activate(
X) →
XTypes:
from :: n__from:n__nil:n__cons
cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
n__from :: n__from:n__nil:n__cons
length :: n__from:n__nil:n__cons → 0':s
n__nil :: n__from:n__nil:n__cons
0' :: 0':s
n__cons :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
s :: 0':s → 0':s
length1 :: n__from:n__nil:n__cons → 0':s
activate :: n__from:n__nil:n__cons → n__from:n__nil:n__cons
nil :: n__from:n__nil:n__cons
hole_n__from:n__nil:n__cons1_0 :: n__from:n__nil:n__cons
hole_0':s2_0 :: 0':s
gen_n__from:n__nil:n__cons3_0 :: Nat → n__from:n__nil:n__cons
gen_0':s4_0 :: Nat → 0':s
Lemmas:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))) → *5_0, rt ∈ Ω(n60)
Generator Equations:
gen_n__from:n__nil:n__cons3_0(0) ⇔ n__from
gen_n__from:n__nil:n__cons3_0(+(x, 1)) ⇔ n__cons(gen_n__from:n__nil:n__cons3_0(x))
gen_0':s4_0(0) ⇔ 0'
gen_0':s4_0(+(x, 1)) ⇔ s(gen_0':s4_0(x))
No more defined symbols left to analyse.
(27) LowerBoundsProof (EQUIVALENT transformation)
The lowerbound Ω(n1) was proven with the following lemma:
length1(gen_n__from:n__nil:n__cons3_0(+(1, n6_0))) → *5_0, rt ∈ Ω(n60)
(28) BOUNDS(n^1, INF)